/-
Copyright (c) 2022 Anne Baanen. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Anne Baanen, Alex J. Best
-/
module

public import Mathlib.Algebra.GroupWithZero.Torsion
public import Mathlib.NumberTheory.RamificationInertia.Galois
public import Mathlib.RingTheory.DedekindDomain.Factorization
public import Mathlib.RingTheory.DedekindDomain.Instances
public import Mathlib.RingTheory.Ideal.Int
public import Mathlib.RingTheory.NormalClosure

/-!

# Ideal norms

This file defines the relative ideal norm `Ideal.spanNorm R (I : Ideal S) : Ideal S` as the ideal
spanned by the norms of elements in `I`.

## Main definitions

* `Ideal.spanNorm R (I : Ideal S)`: the ideal spanned by the norms of elements in `I`.
  This is used to define `Ideal.relNorm`.
* `Ideal.relNorm R (I : Ideal S)`: the relative ideal norm as a bundled monoid-with-zero morphism,
  defined as the ideal spanned by the norms of elements in `I`.

## Main results

* `map_mul Ideal.relNorm`: multiplicativity of the relative ideal norm
* `relNorm_relNorm`: transitivity of the relative ideal norm

-/

@[expose] public section

open scoped nonZeroDivisors

section SpanNorm

namespace Ideal

open Submodule

variable (R S : Type*) [CommRing R] [IsDomain R] {S : Type*} [CommRing S] [IsDomain S]
variable [IsIntegrallyClosed R] [IsIntegrallyClosed S] [Algebra R S] [Module.Finite R S]
variable [NoZeroSMulDivisors R S]

attribute [local instance] FractionRing.liftAlgebra

/-- `Ideal.spanNorm R (I : Ideal S)` is the ideal generated by mapping `Algebra.intNorm R S`
over `I`.

See also `Ideal.relNorm`.
-/
noncomputable def spanNorm (I : Ideal S) : Ideal R :=
  Ideal.map (Algebra.intNorm R S) I

@[simp]
theorem spanNorm_bot :
    spanNorm R (⊥ : Ideal S) = ⊥ := span_eq_bot.mpr fun x hx => by simpa using hx

variable {R} in
@[simp]
theorem spanNorm_eq_bot_iff {I : Ideal S} : spanNorm R I = ⊥ ↔ I = ⊥ := by
  simp only [spanNorm, span_eq_bot, Set.mem_image, SetLike.mem_coe, forall_exists_index, and_imp,
    forall_apply_eq_imp_iff₂, Algebra.intNorm_eq_zero, @eq_bot_iff _ _ _ I, SetLike.le_def, map,
    mem_bot]

theorem intNorm_mem_spanNorm {I : Ideal S} {x : S} (hx : x ∈ I) :
    Algebra.intNorm R S x ∈ I.spanNorm R :=
  subset_span (Set.mem_image_of_mem _ hx)

theorem norm_mem_spanNorm [Module.Free R S] {I : Ideal S} (x : S) (hx : x ∈ I) :
    Algebra.norm R x ∈ I.spanNorm R := by
  refine subset_span ⟨x, hx, ?_⟩
  rw [Algebra.intNorm_eq_norm]

@[simp]
theorem spanNorm_singleton {r : S} :
    spanNorm R (span ({r} : Set S)) = span {Algebra.intNorm R S r} :=
  le_antisymm
    (span_le.mpr fun x hx =>
      mem_span_singleton.mpr
        (by
          obtain ⟨x, hx', rfl⟩ := (Set.mem_image _ _ _).mp hx
          exact map_dvd _ (mem_span_singleton.mp hx')))
    ((span_singleton_le_iff_mem _).mpr (intNorm_mem_spanNorm _ (mem_span_singleton_self _)))

@[simp]
theorem spanNorm_top : spanNorm R (⊤ : Ideal S) = ⊤ := by
  simp [← Ideal.span_singleton_one]

theorem map_spanIntNorm (I : Ideal S) {T : Type*} [Semiring T] (f : R →+* T) :
    map f (spanNorm R I) = span (f ∘ Algebra.intNorm R S '' (I : Set S)) := by
  rw [spanNorm]
  nth_rw 2 [map]
  simp [map_span, Set.image_image]

@[mono]
theorem spanNorm_mono {I J : Ideal S} (h : I ≤ J) : spanNorm R I ≤ spanNorm R J :=
  Ideal.span_mono (Set.monotone_image h)

theorem spanIntNorm_localization (I : Ideal S) (M : Submonoid R) (hM : M ≤ R⁰)
    {Rₘ : Type*} (Sₘ : Type*) [CommRing Rₘ] [Algebra R Rₘ] [CommRing Sₘ] [Algebra S Sₘ]
    [Algebra Rₘ Sₘ] [Algebra R Sₘ] [IsScalarTower R Rₘ Sₘ] [IsScalarTower R S Sₘ]
    [IsLocalization M Rₘ] [IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ]
    [IsIntegrallyClosed Rₘ] [IsDomain Rₘ] [IsDomain Sₘ] [NoZeroSMulDivisors Rₘ Sₘ]
    [Module.Finite Rₘ Sₘ] [IsIntegrallyClosed Sₘ] :
    spanNorm Rₘ (I.map (algebraMap S Sₘ)) = (spanNorm R I).map (algebraMap R Rₘ) := by
  let K := FractionRing R
  let f : Rₘ →+* K := IsLocalization.map _ (T := R⁰) (RingHom.id R) hM
  let L := FractionRing S
  let g : Sₘ →+* L := IsLocalization.map _ (M := Algebra.algebraMapSubmonoid S M) (T := S⁰)
      (RingHom.id S) (Submonoid.map_le_of_le_comap _ <| hM.trans
      (nonZeroDivisors_le_comap_nonZeroDivisors_of_injective _
        (FaithfulSMul.algebraMap_injective _ _)))
  algebraize [f, g, (algebraMap K L).comp f]
  have : IsScalarTower R Rₘ K := IsScalarTower.of_algebraMap_eq'
    (by rw [RingHom.algebraMap_toAlgebra, IsLocalization.map_comp, RingHomCompTriple.comp_eq])
  let _ := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization M Rₘ K
  have : IsScalarTower S Sₘ L := IsScalarTower.of_algebraMap_eq'
    (by rw [RingHom.algebraMap_toAlgebra, IsLocalization.map_comp, RingHomCompTriple.comp_eq])
  have : IsScalarTower Rₘ Sₘ L := by
    apply IsScalarTower.of_algebraMap_eq'
    apply IsLocalization.ringHom_ext M
    rw [RingHom.algebraMap_toAlgebra, RingHom.algebraMap_toAlgebra (R := Sₘ), RingHom.comp_assoc,
      RingHom.comp_assoc, ← IsScalarTower.algebraMap_eq, IsScalarTower.algebraMap_eq R S Sₘ,
      IsLocalization.map_comp, RingHom.comp_id, ← RingHom.comp_assoc, IsLocalization.map_comp,
      RingHom.comp_id, ← IsScalarTower.algebraMap_eq, ← IsScalarTower.algebraMap_eq]
  let _ := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization
    (Algebra.algebraMapSubmonoid S M) Sₘ L
  rw [map_spanIntNorm]
  refine span_eq_span (Set.image_subset_iff.mpr ?_) (Set.image_subset_iff.mpr ?_)
  · intro a' ha'
    simp only [Set.mem_preimage, submodule_span_eq, ← map_spanIntNorm, SetLike.mem_coe,
      IsLocalization.mem_map_algebraMap_iff (Algebra.algebraMapSubmonoid S M) Sₘ,
      IsLocalization.mem_map_algebraMap_iff M Rₘ, Prod.exists] at ha' ⊢
    obtain ⟨⟨a, ha⟩, ⟨_, ⟨s, hs, rfl⟩⟩, has⟩ := ha'
    refine ⟨⟨Algebra.intNorm R S a, intNorm_mem_spanNorm _ ha⟩,
      ⟨s ^ Module.finrank K L, pow_mem hs _⟩, ?_⟩
    simp only [map_pow] at has ⊢
    apply_fun algebraMap _ L at has
    apply_fun Algebra.norm K at has
    simp only [map_mul] at has
    rw [← IsScalarTower.algebraMap_apply, ← IsScalarTower.algebraMap_apply,
      ← IsScalarTower.algebraMap_apply,
      IsScalarTower.algebraMap_apply R K L,
      Algebra.norm_algebraMap] at has
    apply IsFractionRing.injective Rₘ K
    simp only [map_mul, map_pow]
    rwa [Algebra.algebraMap_intNorm (L := L), ← IsScalarTower.algebraMap_apply,
      ← IsScalarTower.algebraMap_apply, Algebra.algebraMap_intNorm (L := L)]
  · intro a ha
    rw [Set.mem_preimage, Function.comp_apply, Algebra.intNorm_eq_of_isLocalization M (Bₘ := Sₘ)]
    exact subset_span (Set.mem_image_of_mem _ (mem_map_of_mem _ ha))

theorem spanNorm_mul_spanNorm_le (I J : Ideal S) :
    spanNorm R I * spanNorm R J ≤ spanNorm R (I * J) := by
  rw [spanNorm, spanNorm, spanNorm]
  nth_rw 1 [map]; nth_rw 1 [map]
  rw [Ideal.span_mul_span', ← Set.image_mul]
  refine Ideal.span_mono (Set.monotone_image ?_)
  rintro _ ⟨x, hxI, y, hyJ, rfl⟩
  exact Ideal.mul_mem_mul hxI hyJ

/-- This condition `eq_bot_or_top` is equivalent to being a field.
However, `Ideal.spanNorm_mul_of_field` is harder to apply since we'd need to upgrade a `CommRing R`
instance to a `Field R` instance. -/
theorem spanNorm_mul_of_bot_or_top (eq_bot_or_top : ∀ I : Ideal R, I = ⊥ ∨ I = ⊤) (I J : Ideal S) :
    spanNorm R (I * J) = spanNorm R I * spanNorm R J := by
  refine le_antisymm ?_ (spanNorm_mul_spanNorm_le R _ _)
  rcases eq_bot_or_top (spanNorm R I) with hI | hI
  · rw [hI, spanNorm_eq_bot_iff.mp hI, bot_mul, spanNorm_bot]
    exact bot_le
  rw [hI, Ideal.top_mul]
  rcases eq_bot_or_top (spanNorm R J) with hJ | hJ
  · rw [hJ, spanNorm_eq_bot_iff.mp hJ, mul_bot, spanNorm_bot]
  rw [hJ]
  exact le_top

theorem spanNorm_le_comap (I : Ideal S) : spanNorm R I ≤ comap (algebraMap R S) I := by
  rw [spanNorm, Ideal.map, Ideal.span_le, ← Submodule.span_le]
  intro x hx
  induction hx using Submodule.span_induction with
  | mem _ h =>
      obtain ⟨x, hx, rfl⟩ := h
      exact mem_comap.mpr <| mem_of_dvd _ (Algebra.dvd_algebraMap_intNorm_self _ _ x) hx
  | zero => simp
  | add _ _ _ _ hx hy => exact Submodule.add_mem _ hx hy
  | smul _ _ _ hx => exact Submodule.smul_mem _ _ hx

/-- Multiplicativity of `Ideal.spanNorm`. simp-normal form is `map_mul (Ideal.relNorm R)`. -/
theorem spanNorm_mul [IsDedekindDomain R] [IsDedekindDomain S] (I J : Ideal S) :
    spanNorm R (I * J) = spanNorm R I * spanNorm R J := by
  nontriviality R
  cases subsingleton_or_nontrivial S
  · have : ∀ I : Ideal S, I = ⊤ := fun I ↦ Subsingleton.elim I ⊤
    simp [this I, this J]
  refine eq_of_localization_maximal (fun P hP ↦ ?_)
  by_cases hP0 : P = ⊥
  · subst hP0
    rw [spanNorm_mul_of_bot_or_top]
    intro I
    exact or_iff_not_imp_right.mpr fun hI ↦ (hP.eq_of_le hI bot_le).symm
  have : NeZero P := ⟨hP0⟩
  let P' := Algebra.algebraMapSubmonoid S P.primeCompl
  simp only [Ideal.map_mul, ← spanIntNorm_localization (R := R) (Sₘ := Localization P')
    _ _ P.primeCompl_le_nonZeroDivisors]
  rw [← (I.map _).span_singleton_generator, ← (J.map _).span_singleton_generator,
    span_singleton_mul_span_singleton, spanNorm_singleton, spanNorm_singleton,
    spanNorm_singleton, span_singleton_mul_span_singleton, map_mul]

section spanNorm_spanNorm

variable (T : Type*) [CommRing T] [IsDomain T] [IsIntegrallyClosed T] [Algebra R T] [Algebra T S]
  [Module.Finite R T] [Module.Finite T S] [NoZeroSMulDivisors R T] [NoZeroSMulDivisors T S]
  [IsScalarTower R T S]

open _root_.Algebra

theorem le_spanNorm_spanNorm (I : Ideal S) : spanNorm R I ≤ spanNorm R (spanNorm T I) := by
  simp_rw [spanNorm, map]
  refine span_mono ?_
  rintro _ ⟨x, hx, rfl⟩
  exact ⟨intNorm T S x, subset_span <| Set.mem_image_of_mem _ hx, by rw [intNorm_intNorm]⟩

/--
This condition `eq_bot_or_top` is equivalent to being a field. However,
`Ideal.spanNorm_spanNorm_of_field` would be harder to apply since we'd need to upgrade
a `CommRing R` instance to a `Field R` instance.
-/
theorem spanNorm_spanNorm_of_bot_or_top (eq_bot_or_top : ∀ I : Ideal R, I = ⊥ ∨ I = ⊤)
    (I : Ideal S) : spanNorm R (spanNorm T I) = spanNorm R I := by
  obtain h | h := eq_bot_or_top (spanNorm R I)
  · rw [h, spanNorm_eq_bot_iff, spanNorm_eq_bot_iff, spanNorm_eq_bot_iff.mp h]
  · exact h ▸ (eq_top_iff_one _).mpr <| le_spanNorm_spanNorm R T I <| (eq_top_iff_one _).mp h

attribute [local instance] Localization.AtPrime.algebra_localization_localization

theorem spanNorm_spanNorm [IsDedekindDomain R] [IsDedekindDomain T] [IsDedekindDomain S]
    (I : Ideal S) : spanNorm R (spanNorm T I) = spanNorm R I := by
  refine eq_of_localization_maximal fun P hP ↦ ?_
  by_cases hP : P = ⊥
  · subst hP
    rw [spanNorm_spanNorm_of_bot_or_top]
    exact fun I ↦ or_iff_not_imp_right.mpr fun hI ↦ (hP.eq_of_le hI bot_le).symm
  let Rₚ := Localization.AtPrime P
  let Tₚ := Localization (algebraMapSubmonoid T P.primeCompl)
  let Sₚ := Localization (algebraMapSubmonoid S P.primeCompl)
  have : NeZero P := ⟨hP⟩
  have h : algebraMapSubmonoid T P.primeCompl ≤ T⁰ :=
      algebraMapSubmonoid_le_nonZeroDivisors_of_faithfulSMul _ (primeCompl_le_nonZeroDivisors P)
  rw [← spanIntNorm_localization R (spanNorm T I) _ (primeCompl_le_nonZeroDivisors P) Tₚ,
    ← spanIntNorm_localization T (Rₘ := Tₚ) I _ h Sₚ, ← spanIntNorm_localization R (Rₘ := Rₚ) I _
    (primeCompl_le_nonZeroDivisors P) Sₚ, ← (I.map _).span_singleton_generator, spanNorm_singleton,
    spanNorm_singleton, intNorm_intNorm, spanNorm_singleton]

end spanNorm_spanNorm

variable [IsDedekindDomain R] [IsDedekindDomain S]

/-- The relative norm `Ideal.relNorm R (I : Ideal S)`, where `R` and `S` are Dedekind domains,
and `S` is an extension of `R` that is finite and free as a module. -/
noncomputable def relNorm : Ideal S →*₀ Ideal R where
  toFun := spanNorm R
  map_zero' := spanNorm_bot R
  map_one' := by rw [one_eq_top, spanNorm_top R, one_eq_top]
  map_mul' := spanNorm_mul R

theorem relNorm_apply (I : Ideal S) :
    relNorm R I = span (Algebra.intNorm R S '' (I : Set S) : Set R) :=
  rfl

@[simp]
theorem spanNorm_eq (I : Ideal S) : spanNorm R I = relNorm R I := rfl

@[simp]
theorem relNorm_bot : relNorm R (⊥ : Ideal S) = ⊥ := by
  simpa only [zero_eq_bot] using map_zero (relNorm R : Ideal S →*₀ _)

@[simp]
theorem relNorm_top : relNorm R (⊤ : Ideal S) = ⊤ := by
  simpa only [one_eq_top] using map_one (relNorm R : Ideal S →*₀ _)

variable {R} in
@[simp]
theorem relNorm_eq_bot_iff {I : Ideal S} : relNorm R I = ⊥ ↔ I = ⊥ :=
  spanNorm_eq_bot_iff

theorem norm_mem_relNorm [Module.Free R S] (I : Ideal S) {x : S} (hx : x ∈ I) :
    Algebra.norm R x ∈ relNorm R I :=
  norm_mem_spanNorm R x hx

@[simp]
theorem relNorm_singleton (r : S) : relNorm R (span ({r} : Set S)) = span {Algebra.intNorm R S r} :=
  spanNorm_singleton R

theorem map_relNorm (I : Ideal S) {T : Type*} [Semiring T] (f : R →+* T) :
    map f (relNorm R I) = span (f ∘ Algebra.intNorm R S '' (I : Set S)) :=
  map_spanIntNorm R I f

@[mono]
theorem relNorm_mono {I J : Ideal S} (h : I ≤ J) : relNorm R I ≤ relNorm R J :=
  spanNorm_mono R h

variable {R}

private theorem relNorm_map_algEquiv_aux {T : Type*} [CommRing T] [IsDedekindDomain T]
    [IsIntegrallyClosed T] [Algebra R T] [Module.Finite R T] [NoZeroSMulDivisors R T]
    (σ : S ≃ₐ[R] T) (I : Ideal S) : relNorm R (I.map σ) ≤ relNorm R I :=
  span_mono fun _ ⟨x, hx₁, hx₂⟩ ↦ ⟨σ.toRingEquiv.symm x,
    by rwa [SetLike.mem_coe, Ideal.symm_apply_mem_of_equiv_iff],
    hx₂ ▸ Algebra.intNorm_map_algEquiv _ x σ.symm⟩

@[simp]
theorem relNorm_map_algEquiv {T : Type*} [CommRing T] [IsDedekindDomain T] [IsIntegrallyClosed T]
    [Algebra R T] [Module.Finite R T] [NoZeroSMulDivisors R T] (σ : S ≃ₐ[R] T) (I : Ideal S) :
    relNorm R (I.map σ) = relNorm R I := by
  refine le_antisymm (relNorm_map_algEquiv_aux σ I) ?_
  convert relNorm_map_algEquiv_aux σ.symm (I.map σ)
  change I = map σ.symm.toAlgHom (map σ.toAlgHom I)
  simp [map_mapₐ]

@[simp]
theorem relNorm_comap_algEquiv {T : Type*} [CommRing T] [IsDedekindDomain T] [IsIntegrallyClosed T]
    [Algebra R T] [Module.Finite R T] [NoZeroSMulDivisors R T] (σ : S ≃ₐ[R] T) (I : Ideal T) :
    relNorm R (I.comap σ) = relNorm R I := map_symm σ.toRingEquiv ▸ relNorm_map_algEquiv σ.symm I

variable (R)

open MulSemiringAction Pointwise in
@[simp]
theorem relNorm_smul {G : Type*} [Group G] [MulSemiringAction G S] [SMulCommClass G R S] (g : G)
    (I : Ideal S) : relNorm R (g • I) = relNorm R I := relNorm_map_algEquiv (toAlgEquiv R S g) I

theorem relNorm_le_comap (I : Ideal S) : relNorm R I ≤ comap (algebraMap R S) I :=
  spanNorm_le_comap R I

theorem relNorm_relNorm (T : Type*) [CommRing T] [IsDedekindDomain T] [IsIntegrallyClosed T]
    [Algebra R T] [Algebra T S] [IsScalarTower R T S] [Module.Finite R T] [Module.Finite T S]
    [NoZeroSMulDivisors R T] [NoZeroSMulDivisors T S]
    (I : Ideal S) : relNorm R (relNorm T I) = relNorm R I :=
  spanNorm_spanNorm _ _ _

variable {R} (S)

attribute [local instance] Localization.AtPrime.liftAlgebra in
theorem relNorm_algebraMap (I : Ideal R) :
    relNorm R (I.map (algebraMap R S)) =
      I ^ Module.finrank (FractionRing R) (FractionRing S) := by
  rw [← spanNorm_eq]
  refine eq_of_localization_maximal (fun P hPd ↦ ?_)
  let P' := Algebra.algebraMapSubmonoid S P.primeCompl
  let Rₚ := Localization.AtPrime P
  let K := FractionRing R
  rw [← spanIntNorm_localization R _ _ P.primeCompl_le_nonZeroDivisors (Localization P'),
      Ideal.map_pow, I.map_map, ← IsScalarTower.algebraMap_eq, IsScalarTower.algebraMap_eq R Rₚ,
      ← I.map_map, ← (I.map _).span_singleton_generator, Ideal.map_span, Set.image_singleton,
      spanNorm_singleton, Ideal.span_singleton_pow]
  congr 2
  apply IsFractionRing.injective Rₚ K
  rw [Algebra.algebraMap_intNorm (L := FractionRing S), ← IsScalarTower.algebraMap_apply,
    IsScalarTower.algebraMap_apply Rₚ K, Algebra.norm_algebraMap, map_pow]

variable (R)

/-- A version of `relNorm_algebraMap` involving a tower of algebras `S/R/R'`. -/
theorem relNorm_algebraMap' {R'} [CommRing R'] (I : Ideal R') [Algebra R' R]
    [Algebra R' S] [IsScalarTower R' R S] : relNorm R (I.map (algebraMap R' S)) =
      I.map (algebraMap R' R) ^ Module.finrank (FractionRing R) (FractionRing S) := by
  rw [← relNorm_algebraMap, Ideal.map_map, IsScalarTower.algebraMap_eq R' R S]

section relNorm_prime

variable {R} {S} (P : Ideal S) (p : Ideal R) [hPp : P.LiesOver p]

/--
See `Ideal.relNorm_eq_pow_of_isMaximal` for a more precise statement when `p` is a maximal ideal.
-/
theorem exists_relNorm_eq_pow_of_isPrime [p.IsPrime] : ∃ s, relNorm R P = p ^ s := by
  by_cases hp : p = ⊥
  · refine ⟨1, ?_⟩
    have : P.LiesOver ⊥ := hp ▸ hPp
    rw [hp, eq_bot_of_liesOver_bot R P, relNorm_bot, bot_pow (one_ne_zero)]
  have h : relNorm R (map (algebraMap R S) p) ≤ relNorm R P :=
    relNorm_mono _ <| map_le_iff_le_comap.mpr <| le_of_eq <| (liesOver_iff _ _).mp hPp
  rw [relNorm_algebraMap S, ← dvd_iff_le, dvd_prime_pow (prime_of_isPrime hp inferInstance)] at h
  obtain ⟨s, _, hs⟩ := h
  exact ⟨s, by rwa [associated_iff_eq] at hs⟩

/--
See `Ideal.relNorm_eq_pow_of_isMaximal` for a statement that does not require the extension to
be Galois.
-/
theorem relNorm_eq_pow_of_isPrime_isGalois [p.IsMaximal] [P.IsPrime]
    [IsGalois (FractionRing R) (FractionRing S)] : relNorm R P = p ^ p.inertiaDeg P := by
  let G := Gal(FractionRing S/FractionRing R)
  let := IsIntegralClosure.MulSemiringAction R (FractionRing R) (FractionRing S) S
  have := IsGaloisGroup.of_isFractionRing G R S (FractionRing R) (FractionRing S)
  by_cases hp : p = ⊥
  · have h : p.inertiaDeg P ≠ 0 := Nat.ne_zero_iff_zero_lt.mpr <| inertiaDeg_pos p P
    have hP : P = ⊥ := by
      rw [hp] at hPp
      exact eq_bot_of_liesOver_bot R P
    rw [hp, hP, relNorm_bot, bot_pow]
    rwa [hp, hP] at h
  obtain ⟨s, hs⟩ := exists_relNorm_eq_pow_of_isPrime P p
  suffices s = p.inertiaDeg P by rwa [this] at hs
  have h₀ : ∀ Q ∈ (p.primesOver S).toFinset,
      relNorm R Q ^ ramificationIdx (algebraMap R S) p Q = p ^ ((p.ramificationIdxIn S) * s) := by
    intro Q hQ
    rw [Set.mem_toFinset] at hQ
    have : Q.IsPrime := hQ.1
    have : Q.LiesOver p := hQ.2
    rw [← ramificationIdxIn_eq_ramificationIdx p Q G]
    obtain ⟨σ, rfl⟩ := Ideal.exists_smul_eq_of_isGaloisGroup p P Q G
    rw [relNorm_smul, hs, ← pow_mul, mul_comm]
  have h := (congr_arg (relNorm R ·) <|
    map_algebraMap_eq_finset_prod_pow hp).symm.trans <| relNorm_algebraMap S p
  simp +contextual only [map_prod, map_pow, h₀, Finset.prod_const, ← pow_mul] at h
  rwa [← IsGaloisGroup.card_eq_finrank G (FractionRing R) (FractionRing S),
    ← Ideal.ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegIn hp S G, mul_comm,
    ← Set.ncard_eq_toFinset_card',
    ((IsLeftCancelMulZero.mul_left_cancel_of_ne_zero hp).pow_injective _).eq_iff,
    mul_right_inj' (primesOver_ncard_ne_zero p S),
    mul_right_inj' (ramificationIdxIn_ne_zero G hp),
    inertiaDegIn_eq_inertiaDeg p P G] at h
  rw [one_eq_top]
  exact IsMaximal.ne_top inferInstance

theorem relNorm_eq_pow_of_isMaximal [PerfectField (FractionRing R)] [P.IsMaximal] [p.IsMaximal] :
    relNorm R P = p ^ p.inertiaDeg P := by
  let T := Ring.NormalClosure R S
  obtain ⟨Q, hQ₁, hQ₂⟩ : ∃ Q : Ideal T, Q.IsMaximal ∧ Q.LiesOver P :=
    exists_maximal_ideal_liesOver_of_isIntegral P
  have : Q.LiesOver p := LiesOver.trans Q P p
  have h := relNorm_eq_pow_of_isPrime_isGalois Q p
  have :  IsGalois (FractionRing S) (FractionRing T) :=
    IsGalois.tower_top_of_isGalois (FractionRing R) (FractionRing S) (FractionRing T)
  rwa [← relNorm_relNorm R S, relNorm_eq_pow_of_isPrime_isGalois Q P, map_pow,
    inertiaDeg_algebra_tower p P Q, pow_mul, pow_left_inj] at h
  exact Nat.ne_zero_iff_zero_lt.mpr <| inertiaDeg_pos P Q

end relNorm_prime

section absNorm

variable [Module.Free ℤ R] [Module.Free ℤ S] [Module.Finite ℤ S]

open UniqueFactorizationMonoid in
theorem absNorm_relNorm [PerfectField (FractionRing R)] (I : Ideal S) :
    absNorm (relNorm R I) = absNorm I := by
  have : Module.Finite ℤ R := Module.Finite.left ℤ R S
  by_cases hI : I = ⊥
  · simp [hI]
  rw [← prod_normalizedFactors_eq_self hI]
  refine Multiset.prod_induction (fun I ↦ absNorm (relNorm R I) = absNorm I) _ ?_ ?_ ?_
  · intro _ _ hx hy
    rw [map_mul, map_mul, map_mul, hx, hy]
  · simp
  · intro Q hQ
    have hQ' : Q ≠ ⊥ := ne_zero_of_mem_normalizedFactors hQ
    rw [Ideal.mem_normalizedFactors_iff hI] at hQ
    have : Q.IsMaximal := Ring.DimensionLEOne.maximalOfPrime hQ' hQ.1
    let P := under R Q
    let p := absNorm (under ℤ P)
    have : NeZero P := ⟨under_ne_bot R hQ'⟩
    have : Q.LiesOver P := by simp [liesOver_iff, P]
    have : Q.LiesOver (span {(p : ℤ)}) := LiesOver.trans Q P _
    have : Fact (p.Prime) := ⟨Nat.absNorm_under_prime _⟩
    have hp : Prime (p : ℤ) := Nat.prime_iff_prime_int.mp <| Nat.absNorm_under_prime _
    rw [relNorm_eq_pow_of_isMaximal Q P, map_pow, absNorm_eq_pow_inertiaDeg Q hp,
      absNorm_eq_pow_inertiaDeg P hp, inertiaDeg_algebra_tower (span {(p : ℤ)}) P Q, pow_mul]

theorem relNorm_int (I : Ideal S) :
    relNorm ℤ I = Ideal.span {(absNorm I : ℤ)} := by
  rw [← Int.ideal_span_absNorm_eq_self (relNorm ℤ I), absNorm_relNorm]

theorem absNorm_algebraMap (I : Ideal R) [Module.Finite ℤ R] :
    absNorm (I.map (algebraMap R S)) =
      (absNorm I) ^ Module.finrank (FractionRing R) (FractionRing S) := by
  rw [← absNorm_relNorm ℤ, ← relNorm_relNorm ℤ R, relNorm_algebraMap, absNorm_relNorm, map_pow]

end absNorm

end Ideal

end SpanNorm
